Search Results

Documents authored by Aiswarya, C.

Found 2 Possible Name Variants:

Aiswarya, C.

Document
DOI: 10.4230/LIPIcs.STACS.2024.5
Satisfiability of Context-Free String Constraints with Subword-Ordering and Transducers

Authors: C. Aiswarya, Soumodev Mal, and Prakash Saivasan

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NExptime-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size 𝒪(n)) and n finite-state automata (each of size 𝒪(n)) can be double exponential in n.
Cite as

C. Aiswarya, Soumodev Mal, and Prakash Saivasan. Satisfiability of Context-Free String Constraints with Subword-Ordering and Transducers. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.STACS.2024.5,
  author =	{Aiswarya, C. and Mal, Soumodev and Saivasan, Prakash},
  title =	{{Satisfiability of Context-Free String Constraints with Subword-Ordering and Transducers}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.5},
  URN =		{urn:nbn:de:0030-drops-197154},
  doi =		{10.4230/LIPIcs.STACS.2024.5},
  annote =	{Keywords: satisfiability, subword, string constraints, context-free, transducers}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.34
Weighted Tiling Systems for Graphs: Evaluation Complexity

Authors: C. Aiswarya and Paul Gastin

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
We consider weighted tiling systems to represent functions from graphs to a commutative semiring such as the Natural semiring or the Tropical semiring. The system labels the nodes of a graph by its states, and checks if the neighbourhood of every node belongs to a set of permissible tiles, and assigns a weight accordingly. The weight of a labeling is the semiring-product of the weights assigned to the nodes, and the weight of the graph is the semiring-sum of the weights of labelings. We show that we can model interesting algorithmic questions using this formalism - like computing the clique number of a graph or computing the permanent of a matrix. The evaluation problem is, given a weighted tiling system and a graph, to compute the weight of the graph. We study the complexity of the evaluation problem and give tight upper and lower bounds for several commutative semirings. Further we provide an efficient evaluation algorithm if the input graph is of bounded tree-width.
Cite as

C. Aiswarya and Paul Gastin. Weighted Tiling Systems for Graphs: Evaluation Complexity. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.FSTTCS.2020.34,
  author =	{Aiswarya, C. and Gastin, Paul},
  title =	{{Weighted Tiling Systems for Graphs: Evaluation Complexity}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.34},
  URN =		{urn:nbn:de:0030-drops-132753},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.34},
  annote =	{Keywords: Weighted graph tiling, tiling automata, Evaluation, Complexity, Tree-width}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.38
Data Multi-Pushdown Automata

Authors: Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We extend the classical model of multi-pushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gap-order constraints that allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. Furthermore, each message inside a stack is equipped with a data item representing its value. When a message is pushed to the stack, its value may be defined by a variable. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in multiple dimensions, namely we have a number of stacks that may contain an unbounded number of messages each of which is equipped with a natural number. It is well-known that the verification of any non-trivial property of multi-pushdown systems is undecidable, even for two stacks and for a finite data-domain. In this paper, we show the decidability of the reachability problem for the classes of data multi-pushdown system that admit a bounded split-width (or equivalently a bounded tree-width). As an immediate consequence, we obtain decidability for several subclasses of data multi-pushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches.
Cite as

Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. Data Multi-Pushdown Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2017.38,
  author =	{Abdulla, Parosh Aziz and Aiswarya, C. and Atig, Mohamed Faouzi},
  title =	{{Data Multi-Pushdown Automata}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{38:1--38:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.38},
  URN =		{urn:nbn:de:0030-drops-78049},
  doi =		{10.4230/LIPIcs.CONCUR.2017.38},
  annote =	{Keywords: Pushdown Systems, Model-Checking, Gap-Order, Bounded Split-Width}
}

Aiswarya, Cyriac

Document
DOI: 10.4230/LIPIcs.CONCUR.2015.340
An Automata-Theoretic Approach to the Verification of Distributed Algorithms

Authors: Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.
Cite as

Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin. An Automata-Theoretic Approach to the Verification of Distributed Algorithms. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 340-353, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.CONCUR.2015.340,
  author =	{Aiswarya, Cyriac and Bollig, Benedikt and Gastin, Paul},
  title =	{{An Automata-Theoretic Approach to the Verification of Distributed Algorithms}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{340--353},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.340},
  URN =		{urn:nbn:de:0030-drops-53737},
  doi =		{10.4230/LIPIcs.CONCUR.2015.340},
  annote =	{Keywords: distributed algorithms, verification, leader election}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact